monad (圈)
triple。餘 standard 構成
圈$ \bf Cに於いて、自己函手$ T:{\bf C}\to{\bf C}と自然變換$ \mu:(T;T)\Rarr T,$ \eta:{\rm Id}_{\bf C}\Rarr Tの組$ (T,\eta,\mu)は、以下を滿たせば monad (圈) と呼ぶ 但し
$ T\muとは各對象$ x_{\in|{\bf C}|}に就いて自然變換$ \muの成分$ \mu_xを函手$ Tに依って移した射$ T(\mu_x)を成分とした自然變換であり、 $ T\mu:=\{T(\mu_x)|\mu_x:(T;T)(x)\to T(x)\}
$ T\eta:=\{T(\eta_x)|\eta_x:x\to T(x)\}
$ \mu Tとは各對象$ x_{\in|{\bf C}|}に就いて自然變換$ \muの對象$ T(x)に於ける成分$ \mu_{T(x)}を成分とした自然變換である $ \mu T:=\{\mu_{T(x)}|\mu_{T(x)}:(T;T)(T(x))\to T(T(x))\}
$ \eta T:=\{\eta_{T(x)}|\eta_{T(x)}:T(x)\to T(T(x))\}
整合條件 (coherence 條件)
可換圖式$ \begin{CD}T;T;T @>T\mu>> T;T \\ @V\mu TVV @VV\mu V \\ T;T @>>\mu > T\end{CD} $ T\mu;\mu=\mu T;\mu
可換圖式$ \begin{CD}T @>T\eta>> T;T \\ @V\eta TVV @VV\mu V \\ T;T @>>\mu> T\end{CD} $ T\eta;\mu={\rm Id}_T=\eta T;\mu
←→餘 monad (comonad。cotriple。standard 構成 (standard construction)) 圈$ \bf Cに於いて、自己函手$ T:{\bf C}\to{\bf C}と自然變換$ \Delta:T\Rarr(T;T),$ \epsilon:T\Rarr{\rm Id}_{\bf C}の組$ (T,\epsilon,\Delta)は、以下を滿たせば 餘 monad と呼ぶ 可換圖式$ \begin{CD}T @>\Delta>> T;T \\ @V\Delta VV @VV\Delta TV \\ T;T @>>T\Delta> T;T;T\end{CD} $ \Delta;\Delta T=\Delta;T\Delta
可換圖式$ \begin{CD}T @>\Delta>> T;T \\ @V\Delta VV @VV\epsilon TV \\ T;T @>>T\epsilon> T\end{CD} $ \Delta;\epsilon T=\Delta;T\epsilon
$ \mathbf{Set}上で單位元附き monoid$ Mをひとつ固定します。 • 左隨伴$ T = (-)\times Mと右隨伴$ G = (-)^M(評價・curry 化の隨伴 (函手)) で$ T \dashv G。 $ \iota_X: X \to (X\times M)^M,\quad \iota_X(x)=\big(m\mapsto (x,m)\big),
$ \kappa_Y: Y^M\times M \to Y,\quad \kappa_Y(f,m)=f(m).
• $ Mを monoid と見ると$ Tは「Writer monad」: $ \eta_X: X\to X\times M,\quad \eta_X(x)=(x,e),\qquad\mu_X: (X\times M)\times M \to X\times M,\ (x,m_1,m_2)\mapsto(x,m_1m_2).
• $ Gは對應する「Reader 餘 monad」:
$ \epsilon_Y: Y^M \to Y,\quad \epsilon_Y(f)=f(e),\qquad\delta_Y: Y^M \to (Y^M)^M,\ \delta_Y(f)(m_1)(m_2)=f(m_1m_2).
ここで $ \eta_X: X\to X\times M と $ \iota_X: X\to (X\times M)^M は型が違ふので一致のしようがなく、$ \epsilon_Y: Y^M\to Y と $ \kappa_Y: Y^M\times M\to Y も同樣に一致しません。
(ただし $ \eta の右 mate として $ \epsilon_Y=\kappa_Y\circ(\eta_{Y^M}) が得られる、といふ「mate 對應」は成り立ちます。)
$ {\bf End}_{\bf C}は函手圈$ {\bf C}^{\bf C}である 對象は圈$ \bf C上の自己函手$ F:{\bf C}\to{\bf C} 恆等函手$ {\rm Id}_{\bf C}を單位 (圈)とする 結合律子は等式が成り立つ$ (F;G);H=F;(G;H)
左右の單位律子は等式が成り立つ$ {\rm Id}_{\bf C};F=F=F;{\rm Id}_{\bf C}
$ \mu:(T;T)\Rarr Tが乘法である
$ \eta:{\rm Id}_{\bf C}\Rarr Tが單位射である
乘法が$ \mu:(T;T)\Rarr Tである
單位射が$ \eta:{\rm Id}_{\bf C}\Rarr Tである
自明な2-圈から2-圈CATへのラックス2-函手である
嚴密 monad
整合條件が自然同型ではなく等式として成り立つ場合を言ふ
$ \mu:(T;T)\Rarr Tを構成する射 (component) が mono 射 maps$ T\eta,\eta T:T\to(T;T)が equal
つまり$ (T,\eta)が well-pointed endofunctor
全ての$ T-代數 (圈) (a.k.a.$ T-module)$ (M,\mu)に於いて$ T-作用$ u:TM\to Mが同型である (卽ち全ての代數 (圈)は不動點である) There exists a pair of adjoint functors$ F\dashv Usuch that the induced monad$ (T:UF,\mu:=U\in F,\eta)is isomorphic to$ (T,\mu,\eta)and$ Uis a 充滿忠實函手である There is a 充滿部分圈$ U:{\bf C}^T\hookrightarrow{\bf C}and a natural bijection of the form$ {\bf C}(T(c),U(a))\to{\bf C}(c,U(a)),(T(c)\xrightarrow{f}U(a))\mapsto(c\xrightarrow{\eta}T(c)\xrightarrow{f}U(a)) The identity natural transformation$ TT\Rarr TTis a distributive law.
しかし、函數型プログラミングの文脈におけるモナドは通常は圏論における強モナドを指すことが多い。
code:unit と bind に依る定義.hs
unit :: x -> M x
bind :: M x -> (x -> M y) -> M y
-- 律
bind (unit x) f == f x
do { y <- f x; return y } == f x
bind m unit == m
do { return m } == m
bind (bind m f) g == bind m (\x -> bind (f x) g)
unit は return とも書く
unit と bind に依る定義は do 糖衣構文にとって自然
code:unit と fmap と join に依る定義.hs
unit :: x -> M x
fmap :: (x -> y) -> M x -> M y
join :: M (M x) -> M x
-- 律
fmap id == id
fmap (f . g) == (fmap f) . (fmap g)
unit . f == fmap f . unit
join . fmap join == join . join
join . fmap unit == join . unit
join . fmap (fmap f) == fmap f . join
code:bind と (fmap, join) との關係.hs
fmap f m == bind m (unit . f)
join m == bind m id
bind m g == join (fmap g m)